Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve verific -chparam and add hierarchy -chparam #871

Merged
merged 7 commits into from
May 6, 2019

Conversation

eddiehung
Copy link
Collaborator

@eddiehung eddiehung commented Mar 13, 2019

  • verific -import -chparam <param> <value> <top_module(s)> now imports top modules from Verific using their original (not parameterised) name
  • verific -import <top_module(s)> now elaborates SV root modules in order to cope with bind statements therein
  • hierarchy -top using Verific is now improved to not elaborate all modules (only specified module, and root modules)
  • Added hierarchy -chparam support (only works for Verific so far)
  • Also more testing in [WIP] Improve verific -chparam and add hierarchy -chparam yosys-tests#16

TODO:

  • hierarchy -chparam ... support for non Verific

@cliffordwolf
Copy link
Collaborator

Do you want me to add non-verific support to hierarchy -chparam?

@eddiehung
Copy link
Collaborator Author

eddiehung commented Mar 14, 2019

Do you want me to add non-verific support to hierarchy -chparam?

If it's a case of calling chparam underneath the hood, then I can fit it in. If there's a more efficient way of doing it, then I'll return to it later.

@cliffordwolf
Copy link
Collaborator

LGTM so far. I'll add the integration with chparam for a read_verilog now.

btw, I've been using this test case as sanity check:

module top #(
        parameter [31:0] X = 0
) (
        input [31:0] din,
        output [31:0] dout
);
        assign dout = X-din;
endmodule

module top_props #(
        parameter [31:0] X = 0
) (
        input [31:0] dout
);      
        always @* assert (dout != X);
endmodule

bind top top_props #(.X(123456789)) props (.*);

with this yosys command:

yosys -p 'verific -sv test.sv; hierarchy -chparam X 123123123 -top top; prep -flatten; sat -prove-asserts -show-ports'

Results are 👍:

Solving problem with 404 variables and 1076 clauses..
SAT proof finished - model found: FAIL!

   ______                   ___       ___       _ _            _ _ 
  (_____ \                 / __)     / __)     (_) |          | | |
   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |
  |  ____/ ___) _ \ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|
  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ 
  |_|   |_|   \___/ \___/ |_|       |_|  \_____|_|\_)_____)\____|_|


  Signal Name             Dec       Hex                                 Bin
  --------------- ----------- --------- -----------------------------------
  \din                -333666  fffae89e    11111111111110101110100010011110
  \dout             123456789   75bcd15    00000111010110111100110100010101

@cliffordwolf
Copy link
Collaborator

My test case for ec39cfd:

module top #(
	parameter [31:0] X = 0
) (
	input [31:0] din,
	output [31:0] dout
);
	assign dout = X-din;
	always @* assert (dout != 123456789);
endmodule

with

yosys -p 'verific -sv test.sv; hierarchy -chparam X 123123123 -top top; prep -flatten; sat -prove-asserts -show-ports'

Removing [WIP]. @eddiehung can you have a quick look? Merge at will.

@cliffordwolf cliffordwolf changed the title [WIP] Improve verific -chparam and add hierarchy -chparam Improve verific -chparam and add hierarchy -chparam May 3, 2019
@eddiehung
Copy link
Collaborator Author

Cursory glance looks okay, though I would like to see a test.

I started some Verific ones here: YosysHQ/yosys-tests#16

Signed-off-by: Clifford Wolf <[email protected]>
@cliffordwolf
Copy link
Collaborator

Added a simple test in d97c644. Merging.

@cliffordwolf cliffordwolf merged commit 7bab7b3 into master May 6, 2019
@cliffordwolf cliffordwolf deleted the verific_import branch May 6, 2019 18:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants